Nuprl Lemma : subtype-fpf
11,40
postcript
pdf
A
:Type,
P
:(
A
),
B
:(
A
Type).
a
:{
a
:
A
|
P
(
a
)} fp
B
(
a
)
r
a
:
A
fp
B
(
a
)
latex
Definitions
parm{i}
Lemmas
subtype-fpf-general
origin
A:Type, P:(A
), B:(AType). a:{a:A| P(a)} fp B(a) 
r a:A fp B(a) A:Type, P:(A), B:(AType). a:{a:A| P(a)} fp B(a) r a:A fp B(a)